Remarks on McCArthy's MTC lecture on Jan 14.

1) I am a strong believer in abstract syntax and I think, that the way to
a really scientific foundation of computer science (or "software science")
leads through the description of our objects using abstract syntax (and
abstract semantics). It seems to me, that most people do not understand
this and pay too much attention to the various problems of concrete
syntax (and semantics).

2) In order to speek about "software objects" in an abstract way, it is
not enough to have the function and predicate apparatus to describe actions
and conditions resp. in flexible levels of abstraction, but a similar
mechanismis needed to describe the data structures too. In FOL the
many-sortedness provides this mechanism, but an attempt to reduce
everything to LISP-type data structures is really a restriction of
generality (not in theoretical sense of course, sinc everything is
expressible with lists, but this may not reflect the real abstract
structure of the object, but is a step towards a more concrete "implementation").

3) The above problem may lead to a not very consequent type of description,
where some aspects of the data structures are described by "nice" functions
(like the operands of a sum), while for the description of others (e.g. if
recursivity is involved) the less abstract LISP  mechanism should be introduced.
(In this sense I find the notation of VDL more convenient, making possible
to describe abstract objects of any complexity and to talk about the components 
of such objects with a functional notation, without committing ourselves
to any kind of concrete structure of represantation. Even VDL objects may
not be general enough for this purpose, but they are - in a practical
sense more general, than lists. And this has nothing to do with other
inconveniences of VDL as a description language or the horribleness of
the first PL/I description). The many-sorted FOL realy has everything,
what is needed to describe abstract data structures in it, may be some
notational concenience ("sugar"?) will be needed to assist this.

4) The lack of a clear description of data structures led to such problems,
whether conditions like isexp(e) why are necessary in some cases and why
not in others. Particularly in constructs like mkecond(p a b) it seems to
be rather important to express the fact, that the type (sort) of the first
argument differs from the others.

5) Some minor remarks and questions:
	a) mkesum can be regarded as a concretisation (I would say "refinement")
of the more abstract concept of mkebinop:
	mkesum(e1 e2) = mkebinop("+" e1 e2)
Mentioning this fact could make the picture a bit more clear.
	b) In the definition of the semantics of an expression, would not be
more appropriate to write
	issum(e) → value(mkesum(value(s1 e,β),value(s2 e,β)))
instead of 
	issum(e) → value(s1 e,β) + value(s2 e,β)
	c) Is x inev in 
		if 0=0 then x else 0 
? According to the definition, not !



REPLY TO MTC.JMC[1,DBX] CONTAINING COMMENTS ON CS258 LECTURE OF 14 JAN 1975


Thanks for your comments on my lecture.  I haven't now anything
concrete to say about your work, but I would be glad to listen
to you for an hour and then comment.  How about Friday afternoon?

1. The choices that I have made so far in abstract syntax do not
commit me to use LISP data structures, and I don't intend to
confine myself to them.  I have not thought much about abstract
data structures, and I consider them part of the semantics.  I
certainly agree that they are desirable.

2. mkebinop is a reasonable way to do it, but since in applications
I have considered so far, including all those put on the board, it
would lengthen the formualas although it would reduce the number
of axioms.

3. I don't see the point of the suggestion concerning the definition
of value(e,β).  We can't do the semantics without introducing +
in the metalanguage so in order to finish the definition I would
still have to treat the case of a sum of numerals.
4. In the sense that I want to use, x is not inevitable in that
expression.  It is need not be for the purpose of reducing
expressions to strong canonical form.  Of course, it would reduce
that expression to x.  However, if we want the fact that 0=0 is
true to be taken into account, where do we draw the line  in knowing
at "syntax time" that an expression will always give the same
truth value.  If we want the definition of inevitability to take
into account all constant expressions, we could define it that way,
but then the concept of inevitable variable would be non-effective,
because in general it is undecideable whether an expression is
constant.

Thanks again for the comments, and if you feel like commenting
on future lectures, please do so, and I'll try to respond.  I
will mention the mkebinop idea which has come up before.